; RUN: %solver %s | %OutputCheck %s
; CHECK-NEXT: ^sat


(set-logic QF_ABV)
(declare-fun v12625 () (_ BitVec 4))
(declare-fun a12629 () (Array (_ BitVec 6) (_ BitVec 9)))
(assert 
(let ((e12630 (_ bv15 6))) 
(let ((e12631 (ite (bvsgt ((_ sign_extend 11) v12625) (_ bv0 15)) (_ bv1 1) (_ bv0 1)))) 
(let ((e12632 (bvand e12630 ((_ zero_extend 5) e12631)))) 
(let ((e12640 (select a12629 (_ bv0 6)))) 
(let ((e12641 (select a12629 e12632))) 
(let ((e12645 (select a12629 ((_ zero_extend 5) e12631)))) 
(let ((e12715 (bvsge (_ bv0 9) e12640))) 
(let ((e12756 (bvult (_ bv0 9) e12645))) 
(let ((e12763 (= (_ bv0 9) e12641))) 
(let ((e12779 (bvsle (_ bv0 6) e12632))) 
(let ((e12799 e12715)) 
(let ((e12830 (ite e12779 true false))) 
(let ((e12842 (= false e12763))) 
(let ((e12863 (not e12799))) 
(let ((e12876 (=> true e12863))) 
(let ((e12884 (not e12842))) 
(let ((e12885 (not e12884))) 
(let ((e12890 e12876)) 
(let ((e12895 (xor false e12885))) 
(let ((e12896 e12895)) 
(let ((e12897 (=> e12890 e12896))) 
(let ((e12898 e12897)) 
(let ((e12899 (not e12898))) 
(let ((e12900 (xor e12830 true))) 
(let ((e12901 (or e12899 e12899))) 
(let ((e12902 (not e12756))) 
(let ((e12903 (not e12902))) 
(let ((e12904 (ite e12900 e12901 e12903))) 
e12904)))))))))))))))))))))))))))))
(check-sat)
